<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>目录</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/qc.css" rel="stylesheet" type="text/css"/>

<script>

$(document).ready(function() {

    $("#accordion").show().accordion({
        autoHeight: false
    });

    $("#accordion div").css({ 'height': 'auto' });
});      


$( function() {
    var icons = {
      header: "ui-icon-circle-arrow-e",
      activeHeader: "ui-icon-circle-arrow-s"
    };
    
    $( "#accordion" ).accordion({
      icons: icons
    });
    $("#accordion").accordion({collapsible : true, active : 'none'});

    $( "#toggle" ).button().on( "click", function() {
      if ( $( "#accordion" ).accordion( "option", "icons" ) ) {
        $( "#accordion" ).accordion( "option", "icons", null );
      } else {
        $( "#accordion" ).accordion( "option", "icons", icons );
      }
    });
  } );
  </script>
<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 4: QuickChick：用 Coq 进行基于性质的测试</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
</ul>
</div>
</a></div>

<div id="main">

<div id="toc">
<div id="accordion">
<h2><a href="Preface.html">Preface</a></h2>
<div>
<ul class="doclist">
<li><a href="Preface.html">页首</a>
<li><a href="Preface.html#lab1">Setup</a>

</li>
<li><a href="Preface.html#lab2">Thanks</a>

</li>
</ul>
</div>
<h2><a href="Introduction.html">Introduction</a></h2>
<div>
<ul class="doclist">
<li><a href="Introduction.html">页首</a>
<li><a href="Introduction.html#lab3">A First Taste of Testing</a>

</li>
<li><a href="Introduction.html#lab6">Overview</a>

</li>
</ul>
</div>
<h2><a href="Typeclasses.html">A Tutorial on Typeclasses in Coq&nbsp;&nbsp;&nbsp;&nbsp;(<b>Typeclasses</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html">页首</a>
<li><a href="Typeclasses.html#lab7">Basics</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab8">Classes and Instances</a>

</li>
<li><a href="Typeclasses.html#lab12">Parameterized Instances: New Typeclasses from Old</a>

</li>
<li><a href="Typeclasses.html#lab15">Class Hierarchies</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab19">How It Works</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab20">Implicit Generalization</a>

</li>
<li><a href="Typeclasses.html#lab21">Records are Products</a>

</li>
<li><a href="Typeclasses.html#lab23">Typeclasses are Records</a>

</li>
<li><a href="Typeclasses.html#lab24">Inferring Instances</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab26">Typeclasses and Proofs</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab27">Propositional Typeclass Members</a>

</li>
<li><a href="Typeclasses.html#lab28">Substructures</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab29">Some Useful Typeclasses</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab30"><span class="inlinecode"><span class="id" type="var">Dec</span></span></a>

</li>
<li><a href="Typeclasses.html#lab33"><span class="inlinecode"><span class="id" type="var">Monad</span></span></a>

</li>
<li><a href="Typeclasses.html#lab34">Others</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab35">Controlling Instantiation</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab36">"Defaulting"</a>

</li>
<li><a href="Typeclasses.html#lab38">Manipulating the Hint Database</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab39">Debugging</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab40">Instantiation Failures</a>

</li>
<li><a href="Typeclasses.html#lab41">Nontermination</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab43">Alternative Structuring Mechanisms</a>

</li>
<li><a href="Typeclasses.html#lab44">Advice from Experts</a>
<div>
<ul class="doclist">
<li><a href="Typeclasses.html#lab45">Matthieu Sozeau</a>

</li>
<li><a href="Typeclasses.html#lab46">John Wiegley</a>

</li>
<li><a href="Typeclasses.html#lab47">Michael Soegtrop</a>

</li>
<li><a href="Typeclasses.html#lab48">Abhishek Anand</a>

</li>
</ul>
</div>

</li>
<li><a href="Typeclasses.html#lab49">Further Reading</a>

</li>
</ul>
</div>
<h2><a href="QC.html">Core QuickChick&nbsp;&nbsp;&nbsp;&nbsp;(<b>QC</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="QC.html">页首</a>
<li><a href="QC.html#lab50">Generators</a>
<div>
<ul class="doclist">
<li><a href="QC.html#lab51">The <span class="inlinecode"><span class="id" type="var">G</span></span> Monad</a>

</li>
<li><a href="QC.html#lab52">Primitive generators</a>

</li>
<li><a href="QC.html#lab54">Lists</a>

</li>
<li><a href="QC.html#lab55">Custom Generators</a>

</li>
<li><a href="QC.html#lab58">Checkers</a>

</li>
</ul>
</div>

</li>
<li><a href="QC.html#lab59">Shrinking</a>
<div>
<ul class="doclist">
<li><a href="QC.html#lab60">Exercise: Ternary Trees</a>

</li>
</ul>
</div>

</li>
<li><a href="QC.html#lab65">Putting it all Together</a>

</li>
<li><a href="QC.html#lab66">Sized Generators</a>

</li>
<li><a href="QC.html#lab68">Automation</a>

</li>
<li><a href="QC.html#lab69">Collecting Statistics</a>

</li>
<li><a href="QC.html#lab70">Dealing with Preconditions</a>
<div>
<ul class="doclist">
<li><a href="QC.html#lab72">Another Precondition: Binary Search Trees</a>

</li>
</ul>
</div>

</li>
</ul>
</div>
<h2><a href="TImp.html">Case Study: a Typed Imperative Language&nbsp;&nbsp;&nbsp;&nbsp;(<b>TImp</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="TImp.html">页首</a>
<li><a href="TImp.html#lab74">Identifiers, Types and Contexts</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab75">Identifiers</a>

</li>
<li><a href="TImp.html#lab77">Types</a>

</li>
<li><a href="TImp.html#lab78">List-Based Maps</a>

</li>
<li><a href="TImp.html#lab79">Deciding <span class="inlinecode"><span class="id" type="var">bound_to</span></span> (optional)</a>

</li>
<li><a href="TImp.html#lab80">Contexts</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab81">Expressions</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab82">Typed Expressions</a>

</li>
<li><a href="TImp.html#lab84">Generating Typed Expressions</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab85">Values and States</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab86">Values</a>

</li>
<li><a href="TImp.html#lab87">States</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab88">Evaluation</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab89">Shrinking for Expressions</a>

</li>
<li><a href="TImp.html#lab90">Back to Soundness</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab91">Well-Typed Programs</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab92">Decidable instance for well-typed.</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab96">Automation (Revisited)</a>
<div>
<ul class="doclist">
<li><a href="TImp.html#lab97">(More) Typeclasses for Generation</a>

</li>
<li><a href="TImp.html#lab98">Using "SuchThat" Typeclasses</a>

</li>
</ul>
</div>

</li>
<li><a href="TImp.html#lab99">Acknowledgements</a>

</li>
</ul>
</div>
<h2><a href="QuickChickTool.html">The QuickChick Command-Line Tool&nbsp;&nbsp;&nbsp;&nbsp;(<b>QuickChickTool</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="QuickChickTool.html">页首</a>
<li><a href="QuickChickTool.html#lab100">Overview</a>

</li>
<li><a href="QuickChickTool.html#lab101">Arithmetic Expressions</a>

</li>
<li><a href="QuickChickTool.html#lab102">QuickChick Test Annotations</a>

</li>
<li><a href="QuickChickTool.html#lab103">Sections</a>

</li>
<li><a href="QuickChickTool.html#lab104">Mutation Testing</a>

</li>
<li><a href="QuickChickTool.html#lab105">A Low-Level Stack Machine</a>

</li>
<li><a href="QuickChickTool.html#lab106">QuickChick Command-Line Tool Flags</a>

</li>
</ul>
</div>
<h2><a href="QuickChickInterface.html">QuickChick Reference Manual&nbsp;&nbsp;&nbsp;&nbsp;(<b>QuickChickInterface</b>)</a></h2>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html">页首</a>
<li><a href="QuickChickInterface.html#lab107">The <span class="inlinecode"><span class="id" type="keyword">Show</span></span> Typeclass</a>

</li>
<li><a href="QuickChickInterface.html#lab108">Generators</a>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html#lab109">Fundamental Types</a>

</li>
<li><a href="QuickChickInterface.html#lab110">Structural Combinators</a>

</li>
<li><a href="QuickChickInterface.html#lab111">Basic Generator Combinators</a>

</li>
<li><a href="QuickChickInterface.html#lab112">Choosing from Intervals</a>

</li>
<li><a href="QuickChickInterface.html#lab113">The <span class="inlinecode"><span class="id" type="var">Gen</span></span> and <span class="inlinecode"><span class="id" type="var">GenSized</span></span> Typeclasses</a>

</li>
<li><a href="QuickChickInterface.html#lab114">Generators for Data Satisfying Inductive Predicates</a>

</li>
</ul>
</div>

</li>
<li><a href="QuickChickInterface.html#lab115">Shrinking</a>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html#lab116">The <span class="inlinecode"><span class="id" type="var">Shrink</span></span> Typeclass</a>

</li>
<li><a href="QuickChickInterface.html#lab117">The <span class="inlinecode"><span class="id" type="var">Arbitrary</span></span> Typeclass</a>

</li>
<li><a href="QuickChickInterface.html#lab118">The Generator Typeclass Hierarchy</a>

</li>
</ul>
</div>

</li>
<li><a href="QuickChickInterface.html#lab119">Checkers</a>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html#lab120">Basic Definitions</a>

</li>
<li><a href="QuickChickInterface.html#lab121">Checker Combinators</a>

</li>
</ul>
</div>

</li>
<li><a href="QuickChickInterface.html#lab122">Decidability</a>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html#lab123">The <span class="inlinecode"><span class="id" type="var">Dec</span></span> Typeclass</a>

</li>
<li><a href="QuickChickInterface.html#lab124">The <span class="inlinecode"><span class="id" type="var">Dec_Eq</span></span> Typeclass</a>

</li>
</ul>
</div>

</li>
<li><a href="QuickChickInterface.html#lab125">Automatic Instance Derivation</a>

</li>
<li><a href="QuickChickInterface.html#lab126">Top-level Commands and Settings</a>

</li>
<li><a href="QuickChickInterface.html#lab127">The <span class="inlinecode"><span class="id" type="var">quickChick</span></span> Command-Line Tool</a>
<div>
<ul class="doclist">
<li><a href="QuickChickInterface.html#lab128">Test Annotations</a>

</li>
<li><a href="QuickChickInterface.html#lab129">Mutant Annotations</a>

</li>
<li><a href="QuickChickInterface.html#lab130">Section Annotations</a>

</li>
<li><a href="QuickChickInterface.html#lab131">Command-Line Tool Flags</a>

</li>
</ul>
</div>

</li>
<li><a href="QuickChickInterface.html#lab132">Deprecated Features</a>

</li>
</ul>
</div>
<h2><a href="PostScript.html">PostScript</a></h2>
<div>
<ul class="doclist">
<li><a href="PostScript.html">页首</a>
<li><a href="PostScript.html#lab133">Future Directions</a>

</li>
<li><a href="PostScript.html#lab134">Recommended Reading</a>

</li>
</ul>
</div>
<h2><a href="Bib.html">Bibliography&nbsp;&nbsp;&nbsp;&nbsp;(<b>Bib</b>)</a></h2>
</div>
</div>

</div>

</div>
</body>
</html>